(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : Set → Set ?1 : ?0 T ?2 : Set ?3 : Id ?2 (?1 tt) _16 : Set [ at Issue903.agda:18,18-32 ] _17 : Set [ at Issue903.agda:18,18-32 ] _19 : Id (?0 T) ?1 [ at Issue903.agda:18,18-32 ] _20 : Id (?0 T) ?1 [ at Issue903.agda:18,18-32 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _19 := e ?2 ?1 ?3 [blocked on problem 25] [25] _16 := T → ?2 [blocked on problem 26] [25, 26] T → ?2 = ?0 T : Set " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3)))
(agda2-give-action 3 "h")
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : Set → Set ?1 : ?0 T ?2 : Set _16 : Set [ at Issue903.agda:18,18-32 ] _17 : Set [ at Issue903.agda:18,18-32 ] _19 : Id (?0 T) ?1 [ at Issue903.agda:18,18-32 ] _20 : Id (?0 T) ?1 [ at Issue903.agda:18,18-32 ] _21 : Id T (?1 tt) [ at 1,1-2 ] _22 : Id T (?1 tt) [ at 1,1-2 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _21 := h [blocked on problem 28] [25, 26] T → T = ?0 T : Set [28, 30] tt = ?1 tt : T _19 := e T ?1 _22 [blocked on problem 25] [25] _16 := T → T [blocked on problem 26] " nil)
((last . 1) . (agda2-goals-action '(0 1 2)))
